Nuprl Lemma : hd_l_interval
11,40
postcript
pdf
T
:Type,
l
:(
T
List),
i
:{0..||
l
||
},
j
:{0..
i
}. hd(l_interval(
l
;
j
;
i
)) =
l
[
j
]
T
latex
Definitions
x
:
A
.
B
(
x
)
,
t
T
,
l
[
i
]
,
nth_tl(
n
;
as
)
,
Y
,
if
b
then
t
else
f
fi
,
i
z
j
,
b
,
i
<z
j
,
tt
,
ff
,
{
i
..
j
}
,
P
Q
,
P
Q
,
i
j
<
k
,
P
&
Q
,
P
Q
,
,
T
,
True
,
A
B
,
A
,
False
Lemmas
int
seg
wf
,
length
wf1
,
select
l
interval
,
le
wf
,
select
wf
,
squash
wf
origin